Inference at * 1 0 1 3 1 
Iof proof for Lemma integer sqrt:



1. n : 
2. 0 < n
3. ((n - 1)  0 )  (r:. (((r * r)  (n - 1)) & ((n - 1) < ((r+1) * (r+1)))))
4. n  0 
  r:. (((r * r)  n) & (n < ((r+1) * (r+1)))) 

latex

 by ((Thin (-1)) 
CollapseTHEN (D (-1))) 

latex

C1: .....antecedent..... NILNIL

C1: 2. 0 < n
C1:   (n - 1)  0 
C2: 

C2: 3. r:. (((r * r)  (n - 1)) & ((n - 1) < ((r+1) * (r+1))))
C2:   r:. (((r * r)  n) & (n < ((r+1) * (r+1))))
C.

Definitions

x:AB(x), P  Q